Add voting, truth predictions, and difficulty ratings to the website#3589
Open
zond wants to merge 1 commit intogoogle-deepmind:mainfrom
Open
Add voting, truth predictions, and difficulty ratings to the website#3589zond wants to merge 1 commit intogoogle-deepmind:mainfrom
zond wants to merge 1 commit intogoogle-deepmind:mainfrom
Conversation
|
Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA). View this failed invocation of the CLA check for more information. For the most up to date status, view the checks section at the bottom of the pull request. |
zond
force-pushed
the
discussions-voting-webtest
branch
10 times, most recently
from
6a9477a to
e32fef5
Compare
…ty ratings Replace the Cloudflare Worker + KV voting backend with GitHub Discussions. Likes are HEART reactions, truth predictions are THUMBS_UP/DOWN reactions, difficulty ratings are discussion comments. A shared App Engine proxy at formal-conjectures-web-worker.uc.r.appspot.com handles OAuth and anonymous reads using GitHub App installation tokens. Key changes: - voting.js: complete rewrite for GitHub Discussions backend - theorem.js/browse.js: enable voting integration and new sort options - appengine/: new App Engine proxy (replaces site/worker/) - build.js: accept pre-processed JSON from the live site - Workflow: -webtest branches skip Lean build, download JSON, inject config - Consent modal on first interaction explaining public nature of activity - OAuth callback routed through proxy so one URL works for all forks Interactive voting widgets are temporarily disabled; read-only discussion data (vote counts, predictions, difficulty) is displayed via the proxy.
zond
force-pushed
the
discussions-voting-webtest
branch
from
e32fef5 to
8530867
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds a GitHub Discussions-backed voting system to the Formal Conjectures website:
All data is stored as native GitHub Discussions features — no separate database.
Architecture
formal-conjectures-web-worker) fetches discussions using GitHub App installation tokensgoogle-deepmind/formal-conjecturesor forks of it*.github.ioorigin automaticallyWhat changed
site/src/js/voting.js— complete rewrite: GitHub Discussions backend, consent modal, truth predictionssite/src/js/theorem.js,browse.js— enable voting integration, new sort optionssite/src/css/style.css— truth widget, consent modal, discussion link stylessite/src/templates/— uncomment voting.js, add sort optionssite/appengine/— new App Engine proxy (replacessite/worker/Cloudflare Worker)site/build.js— accept pre-processed JSON from the live site.github/workflows/build-and-docs.yml—-webtestbranch support, voting config injectionHow to try it
The branch is deployed at https://zond.github.io/formal-conjectures/. Click any theorem, then try voting, predicting, or rating difficulty.
Zero-config for forkers
Branches ending in
-webtestskip the expensive Lean build, download the conjectures JSON from the live site, and deploy to GitHub Pages. To try on your own fork:-webtestNo GCP project, secrets, or tokens needed. See
site/docs/voting.mdfor full details.Test plan
🤖 Generated with Claude Code